(* # ===================================================================
   # Matrix Project
   # Copyright FEM-NUAA.CN 2020
   # =================================================================== *)


(** ** Matrix: A Matrix Type Defined by Record *)

Require Import List.
Require Import Matrix.Mat.list_function.
Require Import Matrix.Mat.Mat_def.
Require Import Matrix.Mat.Mat_make.
Require Import Matrix.Mat.Mat_trans.
Require Import Matrix.Mat.Matrix_Module.
Import ListNotations.

Require Export Setoid.
Require Export Relation_Definitions.
Set Implicit Arguments.

(* ################################################################# *)
(** * Definition of Matrix Type *)

Section Mat_def.
Variable A:Set.
Variable Zero:A.
Variable m n:nat.
Variable f:A->A->A.
Variable f1:A->A.
(** The definition of matrix type requires two relationships as support,
    one is the equivalence relationship of the height of the matrix, 
    and the second is the equivalence relationship of the width of the
    matrix.*)

(** Since we use a two-dimensional list to represent the matrix content,
    where the equivalence of the height of the matrix can be expressed 
    by the height function, the equivalence of the width of the matrix 
    can be expressed by the width function: *)
(*
(** ** height *)
(** height returns Proposition of height relationship of two-dimensional
    list. *)
Definition height2 := @length (list (@Mat A m n)) .

(** ** width *)
(** width returns Proposition of width relationship of two-dimensional
    list. *)
Fixpoint width2 (m:list(list (@Mat A m n))) n2:=
  match m with
  | nil => True
  | a::t => (length a = n2) /\ width2 t n2 
  end.
*)
(** A matrix is a type with parameters whose parameters are the number
    of rows and columns. mkMat is a function of constructing a matrix.
    The construction function requires five parameters: the number of
    rows, the number of columns, the content of the matrix, the number
    of matrix rows, and the number of matrix columns.*)

(** ** Mat *)

Definition Mf:= @matrix_each A f m n.
Definition Mm:= @matrix_map A f1 m n.
Definition mZero := MO A Zero m n.
Definition lmZero := list_o (Mat A m n) mZero.

Fixpoint list_Meq(l1 l2:list(@Mat A m n)):=
  match l1,l2 with
  | hd1::tl1,hd2::tl2 => hd1===hd2 /\list_Meq tl1 tl2
  | nil,nil => True
  | _,_ =>False
  end.

Fixpoint dlist_Meq(dl1 dl2:list(list(@Mat A m n))) :=
  match dl1,dl2 with
  |hd1::tl1,hd2::tl2 => list_Meq hd1 hd2 /\dlist_Meq tl1 tl2
  | nil,nil => True
  | _,_ =>False
  end.


Fixpoint lM_to_M1(l:list (Mat A m n)):=
  match l with
  |nil => nil_list A m 
  |x::x' => mlink A (mat A m n x) (lM_to_M1 x') 
  end.

Lemma height_lM_to_M1: forall l,
  height(lM_to_M1 l) = m.
Proof.
  induction l. - simpl. apply height_nil_list.
  - simpl. apply height_mlink. apply(mat_height A m n a).
    apply IHl. 
Qed.

Lemma width_lM_to_M1: forall n2 l,
  length l = n2 ->
  width (lM_to_M1 l) (n2*n).
Proof.
  - induction n2.
    + induction l. * intros. simpl. apply width_nil_list.
      * intros. inversion H.
    + induction l. * intros. inversion H.
      * intros. simpl. apply width_mlink with(m:=m).
        apply (mat_height A m n a). apply height_lM_to_M1.
        apply (mat_width A m n a). apply IHn2. inversion H.
        auto.
Qed.

Fixpoint dlM_to_M1 (dl1:list( list(@Mat A m n))):=
  match dl1 with 
  | nil => nil
  | x::x' => (lM_to_M1 x )++
     (dlM_to_M1 x' )
  end.

Lemma dlM_to_M1_nil_list:forall m2 ,
  dlM_to_M1 (nil_list(Mat A m n) m2) = nil_list A (m2 *m).
Proof.
  induction m2. simpl. auto.
  simpl. 
  rewrite nil_list_app.
  f_equal. apply IHm2.
Qed.

Lemma height_hd :forall l,
  height (mat A m n (@hd (Mat A m n) mZero l)) = m.
Proof.
  induction l. simpl. apply dlist_o_height.
  simpl. apply (mat_height A m n a). 
Qed.

Lemma length_hd_dl :forall n2 dl,
  width dl n2 ->
  length ((@hd (list(Mat A m n)) (lmZero n2) dl)) = n2.
Proof.
  induction dl. simpl. unfold lmZero. intros. apply list_o_length.
  simpl. intros. apply H.
Qed.

Lemma width_hd :forall l,
  width (mat A m n (@hd (Mat A m n) mZero l))  n.
Proof.
  induction l. simpl. apply dlist_o_width.
  simpl. apply (mat_width A m n a). 
Qed.

Lemma width_tl :forall (B:Set) n2 (dl:list(list B)),
  width dl n2 -> width (tl dl) n2.
Proof.
  induction n2.
  induction dl. auto. intros. simpl. apply H.
  induction dl. intros. simpl. auto. intros.
  simpl. apply H.
Qed.

Lemma height_dlM_to_M1: forall m2 (dl1:list( list(@Mat A m n))),
  height dl1 = m2 -> 
  height (dlM_to_M1 dl1) = m2*m.
Proof.
  induction m2. induction dl1. auto. intros. inversion H.
  induction dl1. intros. inversion H. intros. simpl.
  apply length_app. apply height_lM_to_M1.
  apply IHm2. inversion H. auto.
Qed.


Lemma width_dlM_to_M1: forall n2 (dl1:list( list(@Mat A m n))),
  width dl1 n2 -> width (dlM_to_M1 dl1 ) (n2*n).
Proof.
  induction n2. induction dl1. auto.
  intros. simpl. apply width_app.   
  assert(0=0*n). { auto. } rewrite H0. split.
   apply width_lM_to_M1. apply H.
  apply IHdl1. apply H. induction dl1. intros. simpl. auto.
  intros. simpl. assert(n+n2*n = (S n2)*n). { auto. }
  apply width_app.   rewrite H0. split.
  apply width_lM_to_M1.  apply H.
   apply IHdl1. apply H.
Qed.

Definition MM_to_M'{m2 n2:nat}(ma1:@Mat (@Mat A m n) m2 n2):=
  let ma1':= mat (@Mat A m n) m2 n2 ma1 in
  dlM_to_M1 ma1'.

Lemma height_MM_to_M': forall m2 n2(ma1:@Mat (@Mat A m n) m2 n2),
  height (MM_to_M' ma1) = m2 * m.
Proof.
  intros.
  unfold MM_to_M'. apply height_dlM_to_M1.
  apply (mat_height (@Mat A m n) m2 n2 ma1).
Qed.

Lemma width_MM_to_M':forall m2 n2(ma1:@Mat (@Mat A m n) m2 n2),
  width (MM_to_M' ma1) (n2 * n).
Proof. 
  intros. unfold MM_to_M'. apply width_dlM_to_M1.
  intros. apply(mat_width (@Mat A m n) m2 n2 ma1).
Qed.

Definition MM_to_M{m2 n2}(ma1:@Mat (@Mat A m n) m2 n2):=
  mkMat A (m2*m) (n2*n) (MM_to_M' ma1)
  (height_MM_to_M' ma1) (width_MM_to_M' ma1).


Lemma lM_to_M1_mat_each':forall  n2 ma mb,
  (forall a : A, f a Zero = a)->
  length ma = n2-> length mb = n2 ->
  lM_to_M1 (list_each (Mat A m n) (matrix_each A f) ma mb)  = 
  mat_each' A f (lM_to_M1 ma) (lM_to_M1 mb).
Proof.
  induction n2. - induction ma. + induction mb.
  simpl. rewrite mat_each'_nil_list. auto.
  intros. inversion H1. + intros. inversion H0.
  - induction ma. + intros. inversion H0.
  + induction mb. intros. inversion H1. intros.
  simpl.
  rewrite mat_each'_mlink with(Zero:=Zero)(m:=m)(n:=n)(p:=n2*n).
  f_equal. apply IHn2. auto. inversion H0. auto.
  inversion H1. auto. auto. apply (mat_height A m n a).
  apply height_lM_to_M1. apply (mat_height A m n a0).
  apply height_lM_to_M1. apply (mat_width A m n a).
  apply width_lM_to_M1. inversion H0. auto.
  apply (mat_width A m n a0). apply width_lM_to_M1.
  inversion H1. auto.
Qed.

Lemma dlM_to_M1_mat_each': forall m2 n2 ma mb,
  (forall a, f a Zero = a) ->
  height ma = m2 -> height mb = m2->
  width ma n2-> width mb n2->
  dlM_to_M1 (mat_each' (Mat A m n) (matrix_each A f) ma mb)  =
  mat_each' A f (dlM_to_M1 ma ) (dlM_to_M1 mb ).
Proof.
  induction m2. 
  - induction ma. simpl. auto. intros. inversion H0.
  - induction ma. intros. inversion H0. induction mb. intros.
    inversion H1. intros. simpl. rewrite lM_to_M1_mat_each' with(n2:=n2).
    rewrite mat_each'_app. f_equal. apply IHm2 with(n2:=n2).
    auto. inversion H0. auto. inversion H1. auto. apply H2. apply H3.
    rewrite ?height_lM_to_M1. auto. rewrite ?height_dlM_to_M1 with(m2:=m2).
    auto. inversion H1. auto. inversion H0. auto. auto.
    apply H2. apply H3.
Qed.

Lemma lM_to_M1_list_map : forall la,
  lM_to_M1 (list_map (Mat A m n) (matrix_map A f1) la) 
  = dlist_map A f1 (lM_to_M1 la).
Proof.
  induction la. simpl. rewrite dlist_map_nil_list. auto.
  simpl. rewrite IHla. induction a. unfold matrix_map'. 
  simpl. rewrite dlist_map_mlink with(h:= m).
  auto. auto. apply height_lM_to_M1.
Qed.

Lemma dlM_to_M1_dlist_map: forall  ma,
  dlM_to_M1 (dlist_map (Mat A m n) (matrix_map A f1) ma)  =
  dlist_map A f1 (dlM_to_M1 ma ).
Proof.
  induction ma. 
  - simpl. auto.
  - simpl. rewrite dlist_map_app. f_equal.
  apply lM_to_M1_list_map. apply IHma.
Qed.

Lemma mlink_dlist_o: forall m2 n2 n3,
  mlink A (dlist_o A Zero m2 n2)(dlist_o A Zero m2 n3)
  = dlist_o A Zero m2 (n2+n3).
Proof.
  induction m2. simpl. auto.
  induction n2. simpl. intros. f_equal.
  apply IHm2. induction n3. simpl. f_equal.
  f_equal. rewrite app_nil_r. auto.
  apply IHm2. simpl. f_equal. f_equal. 
  rewrite <- list_o_app. f_equal. apply IHm2.
Qed.

Lemma mlink_dlist_o_lM_to_M1: forall  n2,
  mlink A (dlist_o A Zero m n)
  (lM_to_M1 (list_o (Mat A m n) (MO A Zero m n) n2)) =
  dlist_o A Zero m (n + n2 * n).
Proof.
  induction n2. 
  - simpl. rewrite mlink_nil_list_r. auto.
  apply dlist_o_height.
  - simpl. rewrite IHn2. apply mlink_dlist_o.
Qed.

Lemma lM_to_M1_list_o: forall n2,
  lM_to_M1 (list_o (Mat A m n) (MO A Zero m n) n2)
  = dlist_o A Zero m (n2*n).
Proof.
  induction n2. simpl. rewrite dlist_o_m_0.
  auto. simpl. apply mlink_dlist_o_lM_to_M1.
Qed.

Lemma dlM_to_M1_dlist_o: forall m2 n2 ,
  dlM_to_M1 (dlist_o (Mat A m n) (MO A Zero m n) m2 n2)=
  dlist_o A Zero (m2*m) (n2*n).
Proof.
  induction m2.
  - simpl. auto.
  - induction n2. simpl. rewrite ?dlist_o_m_0.
    rewrite nil_list_app. f_equal. rewrite dlM_to_M1_nil_list.
    auto. simpl. rewrite dlist_o_app. f_equal.
    rewrite lM_to_M1_list_o. apply mlink_dlist_o.
    apply IHm2.
Qed.

Lemma MM_to_M_MO: forall m2 n2,
  MM_to_M (MO (Mat A m n) mZero m2 n2) === MO A Zero (m2*m)(n2*n).
Proof.
  unfold MM_to_M,MM_to_M',MO,M_eq. simpl.
  apply dlM_to_M1_dlist_o.
Qed.

Lemma MM_to_M_matrix_each : forall m2 n2
  (ma mb:Mat(Mat A m n)m2 n2),
  (forall a : A, f a Zero = a) ->
  MM_to_M (matrix_each (Mat A m n) (matrix_each A f) ma mb) ===
  matrix_each A f (MM_to_M ma) (MM_to_M mb).
Proof.
  intros. unfold MM_to_M,MM_to_M',matrix_each,mat_each,M_eq.
  simpl. rewrite dlM_to_M1_mat_each' with(m2:=m2)(n2:=n2).
  auto. auto. apply (mat_height (Mat A m n) m2 n2 ma).
  apply (mat_height (Mat A m n) m2 n2 mb).
  apply (mat_width (Mat A m n) m2 n2 ma).
  apply (mat_width (Mat A m n) m2 n2 mb).
Qed.

Lemma MM_to_M_matrix_map: forall m2 n2
  (ma:Mat(Mat A m n)m2 n2),
  MM_to_M(matrix_map (Mat A m n) (matrix_map A f1) ma) ===
  matrix_map A f1 (MM_to_M ma).
Proof.
  intros. unfold MM_to_M,MM_to_M',matrix_map,matrix_map',M_eq.
  simpl. apply dlM_to_M1_dlist_map.
Qed.

End Mat_def.


Arguments list_Meq {A}{m}{n}.
Arguments dlist_Meq {A}{m}{n}.
Arguments Mf {A}{m}{n}.
Arguments Mm {A}{m}{n}.
Arguments MM_to_M {A}{m}{n}{m2}{n2}.

Section Mat_i.
Variable A:Set.
Variable Zero One:A.

Lemma dlM_to_M1_dlist_i: forall n n2,
  dlM_to_M1 (dlist_i' (Mat A n n) (MO A Zero n n) 
  (MI A Zero One n) n2 n2 0) =
  dlist_i' A Zero One (n2 * n) (n2 * n) 0.
Proof.
  induction n2. simpl. auto.
  simpl.
Admitted.

Lemma MM_to_M_MI: forall n n2,
  MM_to_M (MI (Mat A n n) (MO A Zero n n) (MI A Zero One n) n2) ===
  MI A Zero One (n2*n).
Proof.
  unfold MM_to_M,MM_to_M',M_eq. simpl. Admitted.

End Mat_i. 

Section MM_to_M_validation.

Definition tm1:= mkMat_2_2 1 2 3 4.
Definition tm2:= mkMat_2_2 5 6 7 8.

Definition tm3:= [[tm1;tm2]].
Definition tm4:= [[1;2;5;6];[3;4;7;8]].

Definition tm5:=mkMat_1_2 tm1 tm2 .
Definition tm6:=mkMat_2_4 1 2 5 6 3 4 7 8.

Lemma dlM_to_M_eq: dlM_to_M1 tm3 = tm4.
Proof.
  unfold dlM_to_M1,tm3,tm4. unfold tm1,tm2,lM_to_M1.
  unfold trans,mkMat_2_2,mkMat_2_2'. simpl. auto.
Qed.

Lemma MM_to_M_eq : MM_to_M tm5 === tm6.
Proof.
  unfold MM_to_M,tm5,tm6,M_eq.
  simpl. unfold MM_to_M',mkMat_1_2,tm1,tm2,mkMat_2_4'.
  simpl. auto.
Qed.

End MM_to_M_validation.

Section MM_eq.

Lemma list_Meq_ref: forall A m n(ma:list(@Mat A m n)),
  list_Meq ma ma.
Proof.
  induction ma.
  simpl. apply I. simpl. split. apply M_eq_ref.
  apply IHma.
Qed.

Lemma list_Meq_sym: forall A m n (ma mb:list(@Mat A m n)),
  list_Meq ma mb -> list_Meq mb ma.
Proof.
  induction ma. induction mb.
  simpl. auto. intros. inversion H.
  induction mb. intros. inversion H. 
  simpl. intros. inversion H. rewrite H0. split.
  apply M_eq_ref. apply IHma. apply H1.
Qed.

Lemma list_Meq_trans:forall A m n (ma mb mc:list(@Mat A m n)),
  list_Meq ma mb -> list_Meq mb mc -> list_Meq ma mc.
Proof.
 induction ma.
  - induction mb. 
    + induction mc. auto. auto. 
    + intros. inversion H.
  - induction mb.
    + intros. inversion H.
    + induction mc.
      intros. inversion H0. simpl. intros. inversion H.
      inversion H0. rewrite H1. split. apply H3. apply IHma with(mb:=mb).
      apply H2. apply H4.
Qed.

Lemma lMeq_ref : forall {A:Set} {m n:nat}, reflexive _ (@list_Meq A m n).
Proof.  intros. unfold reflexive. apply list_Meq_ref. Qed.

Lemma lMeq_sym : forall {A:Set} {m n:nat}, symmetric _ (@list_Meq A m n).
Proof. intros. unfold symmetric. apply list_Meq_sym. Qed.

Lemma lMeq_trans : forall {A:Set} {m n:nat}, transitive _ (@list_Meq A m n).
Proof. intros. unfold transitive. apply list_Meq_trans. Qed.

Add Parametric Relation {A:Set} {m n:nat} : (list(@Mat A m n)) (@list_Meq A m n) 
  reflexivity proved by (@lMeq_ref A m n)
  symmetry proved by (@lMeq_sym A m n )
  transitivity proved by (@lMeq_trans A m n )
  as lMeq_rel.

Lemma dlist_Meq_ref: forall A m n (ma:list(list(@Mat A m n))),
  dlist_Meq ma ma.
Proof.
  induction ma.
  simpl. apply I. simpl. split. reflexivity. apply IHma.
Qed.

Lemma dlist_Meq_sym: forall A m n (ma mb:list(list(@Mat A m n))),
  dlist_Meq ma mb -> dlist_Meq mb ma.
Proof. 
  induction ma,mb.
  - auto. - auto. - auto. - simpl. intros. inversion H. rewrite H0. split.
  reflexivity. apply IHma. apply H1.
Qed.

Lemma dlist_Meq_trans: forall A m n (ma mb mc:list(list(@Mat A m n))),
  dlist_Meq ma mb -> dlist_Meq mb mc -> dlist_Meq ma mc.
Proof.
  induction ma.
  - induction mb.
    + induction mc.
      * intros. auto. * intros. inversion H0.
    + intros. inversion H.
  - induction mb.
    + intros. inversion H.
    + induction mc.
      * intros. inversion H0.
      * intros. simpl. inversion H. inversion H0.
      rewrite H1. split. apply H3. apply IHma with(mb:=mb).
      apply H2. apply H4.
Qed.

Lemma dlMeq_ref : forall {A:Set} {m n:nat}, reflexive _ (@dlist_Meq A m n).
Proof.  intros. unfold reflexive. apply dlist_Meq_ref. Qed.

Lemma dlMeq_sym : forall {A:Set} {m n:nat}, symmetric _ (@dlist_Meq A m n).
Proof. intros. unfold symmetric. apply dlist_Meq_sym. Qed.

Lemma dlMeq_trans : forall {A:Set} {m n:nat}, transitive _ (@dlist_Meq A m n).
Proof. intros. unfold transitive. apply dlist_Meq_trans. Qed.

Add Parametric Relation {A:Set} {m n:nat} : (list(list(@Mat A m n))) (@dlist_Meq A m n) 
  reflexivity proved by (@dlMeq_ref A m n)
  symmetry proved by (@dlMeq_sym A m n )
  transitivity proved by (@dlMeq_trans A m n )
  as dlMeq_rel.

(** * Definition of Matrix Equality*)


Definition MM_eq{A:Set} {m n m2 n2:nat} (ma mb:@Mat (@Mat A m n) m2 n2 ):= 
  dlist_Meq (mat (@Mat A m n) m2 n2 ma) (mat (@Mat A m n) m2 n2 mb).

(** Use the symbol === to express M_eq *)

Notation "m1 == m2" := (MM_eq m1 m2) (at level 70).

(** ** Lemmas of M_eq *)

(** Proof of reflexivity of M_eq *)

Lemma MM_eq_ref : forall {A:Set} {m n m2 n2:nat} (m0:@Mat (@Mat A m n) m2 n2),
   m0 == m0.
Proof. intros.
  induction m0.
  unfold MM_eq. simpl. apply dlist_Meq_ref.
Qed.

(** Proof of symmetry of M_eq *)

Lemma MM_eq_sym : forall {A:Set} {m n m2 n2:nat} 
  (m0 m1:@Mat (@Mat A m n) m2 n2), 
  m0 == m1 -> m1 == m0.
Proof. intros. unfold MM_eq in H. unfold MM_eq. rewrite H. reflexivity.
Qed.

(** Proof of transitivity of M_eq *)

Lemma MM_eq_trans : forall {A:Set} {m n m2 n2:nat}
  (m0 m1 m2:@Mat (@Mat A m n) m2 n2),
  m0 == m1 -> m1 == m2 -> m0 == m2.
Proof. intros. unfold MM_eq in H. unfold MM_eq in H0.
  unfold MM_eq . rewrite H. rewrite <- H0. reflexivity.
Qed.

(** * Implementation of M_eq rewrite *)



Lemma MMeq_ref : forall {A:Set} {m n m2 n2:nat}, reflexive _ (@MM_eq A m n m2 n2).
Proof.  intros. unfold reflexive. apply MM_eq_ref. Qed.

Lemma MMeq_sym : forall {A:Set} {m n m2 n2:nat}, symmetric _ (@MM_eq A m n m2 n2).
Proof. intros. unfold symmetric. apply MM_eq_sym. Qed.

Lemma Meq_trans : forall {A:Set} {m n m2 n2:nat}, transitive _ (@MM_eq A m n m2 n2).
Proof. intros. unfold transitive. apply MM_eq_trans. Qed.

Add Parametric Relation {A:Set} {m n m2 n2:nat} : 
  (@Mat (@Mat A m n) m2 n2) (@MM_eq A m n m2 n2) 
  reflexivity proved by (@MM_eq_ref A m n m2 n2)
  symmetry proved by (@MM_eq_sym A m n m2 n2)
  transitivity proved by (@MM_eq_trans A m n m2 n2)
  as MM_eq_rel.

Lemma lM_to_M1_eq_l1: forall A m n
  (la lb:list (Mat A m n)),
  list_Meq la lb ->
  lM_to_M1 la = lM_to_M1 lb.
Proof.
  induction la,lb. simpl. auto.
  intros. inversion H. intros. inversion H.
  intros. simpl. f_equal. simpl in H. 
  inversion H. apply H0. apply IHla. inversion H.
  auto.
Qed.

Lemma dlM_to_M1_eq_dl1: forall A m n 
  (ma mb:list (list  (Mat A m n))),
  dlist_Meq ma mb ->
  dlM_to_M1 ma = dlM_to_M1 mb.
Proof.
  induction ma. induction mb. simpl. auto.
  intros. inversion H. induction mb. intros.
  inversion H. intros. simpl. f_equal.
  inversion H. apply lM_to_M1_eq_l1. auto.
  inversion H. auto.
Qed.

Lemma MM_to_M_M_eq1: forall A m n m2 n2 
  (ma mb:Mat (Mat A m n) m2 n2),
  ma == mb ->
  MM_to_M ma === MM_to_M mb.
Proof.
  intros. induction ma,mb. unfold M_eq,MM_to_M,MM_to_M'. simpl.
  apply dlM_to_M1_eq_dl1. unfold MM_eq in H. simpl in H.
  auto.
Qed. 

Lemma app_eq_l: forall (A:Set) h1 h2(a a1 a2 a3:list A),
  length a = h1 ->length a2 = h1 ->
  length a1 = h2 ->length a3 = h2 ->
  a ++ a1 = a2 ++ a3 ->
  a = a2 /\ a1 = a3. 
Proof.  
  induction h1.
  induction a,a2. simpl. auto.
  intros. inversion H0. intros. inversion H.
  intros. inversion H.
  induction h2.
  induction a1. induction a3. simpl. intros.
  rewrite ?app_nil_r in H3. split. auto. auto.
  intros. inversion H2. intros. inversion H1.
  induction a. intros. inversion H.
  induction a2. intros. inversion H0.
  induction a1. intros. inversion H1.
  induction a5. intros. inversion H2.
  intros. simpl in H3. inversion H3.
  apply IHh1 with(h2:= S h2) in H6.
  split. f_equal. apply H6. apply H6.
  inversion H. auto. inversion H0. auto.
  auto. auto.
Qed.
 
Lemma mlink_eq_l: forall A h w1 w2 a b c d,
  height a = h -> height b = h ->
  height c = h -> height d = h ->
  width a w1 -> width c w1 ->
  width b w2 -> width d w2 ->
  mlink A a b = mlink A c d ->
  a =c /\b = d.
Proof.
  induction h.
  - induction a. induction b. induction c. induction d.
    simpl. auto. intros. inversion H2. intros. inversion H1.
    intros. inversion H0. intros. inversion H. 
  - induction a. intros. inversion H.
    induction b. intros. inversion H0.
    induction c. intros. inversion H1.
    induction d. intros. inversion H2.
    intros. simpl in H7. inversion H7. assert(a0 = c/\ b = d).
    { apply IHh with(w1:=w1)(w2:=w2). inversion H. auto.
      inversion H0. auto. inversion H1. auto. inversion H2.
      auto. apply H3. apply H4. apply H5. apply H6.
      auto. } split. 
    apply app_eq_l with(h1:=w1)(h2:=w2) in H9.
    inversion H9. rewrite H11. f_equal. apply H8. 
    apply H3. apply H4. apply H5. apply H6.
    apply app_eq_l with(h1:=w1)(h2:=w2) in H9. 
    inversion H9. rewrite H12. f_equal.
    apply H8.  apply H3. apply H4. apply H5. apply H6.
Qed.

Lemma lM_to_M1_eq_l2: forall A m n h
  (la lb:list (Mat A m n)),
  length la = h -> length lb = h ->
  lM_to_M1 la = lM_to_M1 lb ->
  list_Meq la lb .
Proof.
  induction h.
  induction la. induction lb. simpl. auto.
  intros. inversion H0. intros. inversion H.
  induction la. intros. inversion H. induction lb.
  intros. inversion H0. intros. simpl.
  simpl in H1. apply mlink_eq_l with(h:=m)(w1:=n)(w2:=h*n)in H1 .
  inversion H1. split. apply H2. apply IHh. inversion H.
  auto. inversion H0. auto. auto.
  apply (mat_height A m n a). apply height_lM_to_M1.
  apply (mat_height A m n a0). apply height_lM_to_M1.
  apply (mat_width A m n a). apply (mat_width A m n a0).
  apply width_lM_to_M1. inversion H. auto.
  apply width_lM_to_M1. inversion H0. auto.
Qed.

Lemma dlM_to_M1_eq_dl2: forall A m n h w
  (ma mb:list (list  (Mat A m n))),
  height ma = h-> height mb =h ->
  width ma w -> width mb w->
  dlM_to_M1 ma = dlM_to_M1 mb ->
  dlist_Meq ma mb.
Proof.
  induction h. 
  - induction ma. induction mb. simpl. auto.
    intros. inversion H0. intros. inversion H.
  - induction ma. intros. inversion H.
    induction mb. intros. inversion H0.
    intros. simpl. simpl in H3. 
    apply app_eq_l with(h1:= m)(h2:=h*m)in H3 .
    inversion H3. split. apply lM_to_M1_eq_l2 with(h:=w).
    apply H1. apply H2. auto. apply IHh with(w:=w).
    inversion H. auto. inversion H0. auto.
    apply H1. apply H2. auto. apply height_lM_to_M1.
    apply height_lM_to_M1. apply height_dlM_to_M1.
    inversion H. auto. apply height_dlM_to_M1. 
    inversion H0. auto.
Qed.


Lemma MM_to_M_M_eq2: forall A m n m2 n2 
  (ma mb:Mat (Mat A m n) m2 n2),
  MM_to_M ma === MM_to_M mb ->
  ma == mb .
Proof.
  induction ma,mb. unfold M_eq,MM_eq,MM_to_M,MM_to_M'. simpl.
  apply dlM_to_M1_eq_dl2 with(h:=m2)(w:=n2).
  auto. auto. auto. auto.
Qed.

Lemma MM_to_M_M_eq: forall A m n m2 n2 
  (ma mb:Mat (Mat A m n) m2 n2),
  ma == mb <->
  MM_to_M ma === MM_to_M mb.
Proof.
  split. apply MM_to_M_M_eq1. apply MM_to_M_M_eq2.
Qed.


Definition matA (A:Set)(m n m2 n2:nat) := @Mat (@Mat A m n) m2 n2.
Parameters mat_add : forall (A:Set) m n m2 n2, 
  (@Mat (@Mat A m n) m2 n2) ->
  (@Mat (@Mat A m n) m2 n2) ->
  (@Mat (@Mat A m n) m2 n2) .

Axiom mat_add_compat : 
  forall (A:Set) m n m2 n2, 
     forall x x' : (@Mat (@Mat A m n) m2 n2), @MM_eq A m n m2 n2 x x' ->
     forall y y' : (@Mat (@Mat A m n) m2 n2), @MM_eq A m n m2 n2 y y' ->
         @MM_eq A m n m2 n2(mat_add x y) (mat_add x' y').

Add Parametric Morphism {A:Set} {m n m2 n2 :nat}: (@mat_add A m n m2 n2)
  with signature (@MM_eq A m n m2 n2) ==> (@MM_eq A m n m2 n2) ==> (@MM_eq A m n m2 n2) 
  as mat_add_mor.
Proof.
exact (@mat_add_compat A m n m2 n2).
Qed.

Section test.
Variable A:Set.
Variable m1 m2 m3 m4 m5:@Mat (@Mat A  3 3) 2 2.
Axiom t1: mat_add m1 m2 == m3.
Axiom t2: m2 == mat_add m4 m5.
Lemma t3: mat_add m1 m2 == mat_add m1 (mat_add m4 m5).
Proof.
  rewrite t2. reflexivity.
Qed.
End test.

End MM_eq.

Notation "m1 == m2" := (MM_eq m1 m2) (at level 70).

